#!/bin/bash
set -x

# if [ -z ${ROOTDIR+x} ]; then ROOTDIR=$(git rev-parse --show-toplevel); fi


help="This script calls the lv6 compiler to generate kind2 compatible lustre

usage:
  $0 [[[property] [int]] [solver]]

where:
  - property is one of the verify node variable (in verify.lus) (ok by default)
  - int is in {int, int8, uint8, int16, uint16, ..., uinit64} [2] (int8+ by default)
  - solver is in {Z3, Bitwuzla, cvc5, MathSAT, Yices, Yices2} [3] (Bitwuzla by default)


[2] int means natural numbers (infinite)
  uint8  : 0 to 255
  uint16 : 0 to 65535
  uint32 : 0 to 4294967295
  uint64 : 0 to 18446744073709551615
  int8   : -128 to 127
  int16  : -32768 to 32767
  int32  : -2147483648 to 2147483647
  int64  : -9223372036854775808 to 9223372036854775807
[3] cf kind2 documentation
"

kind2 --version || { echo "kind2 is not installed. try: opam install kind2" ; exit 2; }

int=int8
solver=Bitwuzla
prop=ok

#### Dealing with CL arguments
# at least 2 arguments are required
#    if [[ $# < 2 ]]
#    then
#        printf "$help"
#        exit 2
#    elif [[ $# == 2 ]]
#    then
#       main=$1$2
#       prop=ok
#       daemon=distributed
#       int=int8
#       solver=Z3
#       shift
#       shift
#    elif [[ $# == 3 ]]
#    then
#       topology=$1
#       n=$2
#       main=$1$2
#       prop=$3
#       daemon=distributed
#       int=int8
#       solver=Z3
#       shift
#       shift
#       shift
#    elif [[ $# == 4 ]]
#    then
#       topology=$1
#       n=$2
#       main=$1$2
#       prop=$3
#       daemon=$4
#       int=int8
#       solver=Z3
#       shift
#       shift
#       shift
#       shift
#    elif [[ $# == 5 ]]
#    then
#       topology=$1
#       n=$2
#       main=$1$2
#        prop=$3
#        daemon=$4
#        int=$5
#        solver=$6
#        shift
#        shift
#        shift
#        shift
#        shift
#    else
#       topology=$1
#       n=$2
#       main=$1$2
#       prop=$3
#       daemon=$4
#       int=$5
#       solver=$6
#       shift
#       shift
#       shift
#       shift
#        shift
#        shift
#  fi


# if [ -z ${TIMEOUT} ]; then TIMEOUT=194400.; fi # n: 194400s = 54 hours (2,3 jours)
if [ -z ${TIMEOUT} ]; then TIMEOUT=1944000.; fi # n: 1944000s = 540 hours (23 jours)
if [ -z ${kind2_opt_more} ]; then kind2_opt_more="--modular true --compositional true"; fi


#### playing with kind2 options
kind2_opt="--timeout 36000 -json -v "
kind2_opt="--enable BMC --enable IND --timeout 36000 -json -v"
kind2_opt="--enable BMC --enable IND --enable IC3 --timeout 36000"
kind2_opt="--exit_code_mode results_and_errors --smt_solver $solver --enable BMC --enable IND ${kind2_opt_more} --timeout ${TIMEOUT} "

# --qe_method {precise|impl|cooper}

# work in a tmp dir to ease the cleaning
#  TMP=.tmp-`uname -n`
#  [ -d ${TMP} ] || mkdir ${TMP}
#  cp *.lus ${TMP}
#  cd ${TMP}

start0=`date +%s.%N`


main=proove_me
options="-eei  --lustre-v4 -np -knc -knpc --assert-in-contract"

# Get rif of the lutre v6 constructs that kind2 does not handle
lv6 $@ $options -o $main.verify.lv4 || ( echo "lv6 $@ $options  failed"; exit 2 )

# set the property to check
cat $main.verify.lv4 | sed -e "s/--%PROPERTY \(.*\);/--%PROPERTY $prop;/g"  > $main.verify.lv4.tmp
mv $main.verify.lv4.tmp $main.verify.lv4

# using machine integers instead of int: eg, replace 42 by (uint8 42)

cat $main.verify.lv4 | \
    sed -r "s/([ \t\r\n=([<>\/\*\+]+)((-)?[[:digit:]]+)/ \1(${int} \2)/g" | \
    sed -r "s/:int/:${int}/g" \
    > $main.verify.${int}.lv4

pb="|"
start=`date +%s.%N`
time kind2 --color true ${kind2_opt} $main.verify.${int}.lv4 || pb="|ZZZ_kind_failed!!! "
end=`time date +%s.%N`
wallclock0=$( echo "$end - $start0" | bc -l )
wallclock=$( echo "$end - $start" | bc -l )

timestamp=`date +"%d/%m/%Y-%H:%M:%S"`
algodir=$(dirname $PWD)
algo=$(basename $algodir)

LC_NUMERIC="en_US.UTF-8"

# let's keep a track of all runs (it can expensive, it should not be lost)
# in a .org file
ALL_RESULT="lv6-result-`uname -n`.org"
printf "%s | %.2f-%.2f | %s | %s | %s | %s |\n" $pb  \
      $wallclock0 $wallclock $int $solver $timestamp `kind2 --version | cut -d ' ' -f2` >> ${ALL_RESULT}

echo "cf ${ALL_RESULT}"

if [ "$pb" = "|" ]; then
    echo "kind2 proved the property."
else
    exit 2
fi